(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
proper(c) → ok(c)
proper(f(X)) → f(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 6.
The certificate found is represented by the following graph.
Start state: 11
Accept states: [12]
Transitions:
11→12[active_1|0, proper_1|0, f_1|0, g_1|0, top_1|0]
11→13[mark_1|1]
11→16[ok_1|1]
11→17[ok_1|1]
11→18[ok_1|1]
11→19[top_1|1]
11→20[top_1|1]
11→21[top_1|2]
11→22[top_1|2]
11→27[top_1|3]
11→35[top_1|3]
11→39[top_1|4]
11→40[top_1|4]
11→43[top_1|5]
11→45[top_1|5]
11→48[top_1|6]
12→12[c|0, mark_1|0, ok_1|0]
13→14[f_1|1]
14→15[g_1|1]
15→12[c|1]
16→12[c|1]
17→12[f_1|1]
17→17[ok_1|1]
18→12[g_1|1]
18→18[ok_1|1]
19→12[proper_1|1]
19→16[ok_1|1]
20→12[active_1|1]
20→13[mark_1|1]
21→16[active_1|2]
21→23[mark_1|2]
22→13[proper_1|2]
22→26[f_1|2]
22→33[ok_1|3]
23→24[f_1|2]
24→25[g_1|2]
25→12[c|2]
26→14[proper_1|2]
26→28[g_1|2]
26→31[ok_1|3]
27→23[proper_1|3]
27→29[f_1|3]
27→37[ok_1|4]
28→15[proper_1|2]
28→30[ok_1|2]
29→24[proper_1|3]
29→32[g_1|3]
29→36[ok_1|4]
30→12[c|2]
31→30[g_1|3]
32→25[proper_1|3]
32→34[ok_1|3]
33→31[f_1|3]
34→12[c|3]
35→33[active_1|3]
35→38[mark_1|4]
36→34[g_1|4]
37→36[f_1|4]
38→30[g_1|4]
39→37[active_1|4]
39→41[mark_1|5]
40→38[proper_1|4]
40→42[g_1|5]
40→36[ok_1|4]
41→34[g_1|5]
42→30[proper_1|5]
42→34[ok_1|3]
43→41[proper_1|5]
43→44[g_1|6]
43→47[ok_1|5]
44→34[proper_1|6]
44→46[ok_1|4]
45→36[active_1|5]
46→12[c|4]
47→46[g_1|5]
48→47[active_1|6]